1. Field of the Invention
The present invention relates in general to verifying circuit designs and in particular to representing a logic function of a circuit design in a binary decision diagram. Still more particularly, the present invention relates to a system, method and computer-readable medium for building binary decision diagrams for nodes in a netlist representation of a circuit design more optimally and performing on-demand variable quantification using case-splitting.
2. Description of the Related Art
Many tasks in computer-aided design (CAD) of digital circuits, such as equivalence checking, property checking, logic synthesis, false-paths analysis require Boolean reasoning on problems derived from circuit structures. A netlist graph is a means for representing problems derived from these circuit structures. Such a representation is non-canonical and offers limited ability to reason about the function at the nodes in the graph. Binary decision diagrams (BDDs) can be used for efficiently applying Boolean reasoning to problems derived from such circuit structures. A BDD offers a compact and functionally canonical representation of the Boolean function of a node in the netlist graph, which makes it easy and fast to reason about its function.
Unfortunately, the size of BDDs, and the complexity involved with manipulating them, is very sensitive to the order in which variables appear in the BDDs. This sensitivity to variable ordering can result in exponential space complexity of the BDD. BDD packages that implement BDD building and manipulation algorithms use Dynamic Variable Ordering (DVO) algorithms to reduce the number of BDD nodes periodically. These algorithms tend to be expensive in both time and space complexity. Therefore, BDD software packages rely on heuristics to compute a local minimum as opposed to a global minimum for reducing the number of BDD nodes, since computing a global minimum is prohibitively expensive in space as well as in time. Starting with a good initial order and computing a good order when the number of BDD nodes is relatively small is strongly suggested. Many applications set an upper limit on the number of allowed BDD nodes to prevent a “runaway” BDD operation. The upper limit can be on the number of BDDs allowed to exist at any point in time in a BDD package due to the data structures used, or due to the available memory of the computer system on which the BDD package is running. The presence of spurious BDDs may cause this limit to be hit prematurely and make a big difference in whether the computation is able to be completed.
Additionally, it may be the case that the application requiring the building of BDDs may need to quantify certain variables, for example when performing symbolic model checking. Typical quantification approaches build the BDDs to completion before resorting to quantification of the variables and are therefore prone to memory overruns during their BDD-building phase.